Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		2nd(cons1(X,cons(Y,Z)))	→ Y
2:		2nd(cons(X,X1))	→ 2nd(cons1(X,activate(X1)))
3:		from(X)	→ cons(X,n__from(s(X)))
4:		from(X)	→ n__from(X)
5:		activate(n__from(X))	→ from(X)
6:		activate(X)	→ X

There are 3 dependency pairs:


7:		2nd#(cons(X,X1))	→ 2nd#(cons1(X,activate(X1)))
8:		2nd#(cons(X,X1))	→ ACTIVATE(X1)
9:		ACTIVATE(n__from(X))	→ FROM(X)

The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 3, 2006